fix(798): trap Int/Nat arithmetic overflow + Tier-1 obligation (v0.0.181)#809
Merged
Conversation
…181)
vera verify modelled Int/Nat as Z3 unbounded integers, so +, -, and *
were total — it proved postconditions the i64/u64 runtime violated under
two's-complement wraparound (ensures(result > x) for { x + 1 } verified at
Tier 1, yet inc(i64.MAX) wraps to i64.MIN). Overflow was the one
partial-arithmetic case treated as total by both tiers; Nat underflow and
signed-division MIN/-1 already trap.
Int/Nat +, -, and * are now partial operations that trap on overflow at
runtime, with an auto-synthesised int_overflow obligation that the result
stays in i64/u64 range — a two-check mirroring array bounds (#680):
provably in range -> Tier 1; provably out of range -> compile error E528;
dynamic operands -> runtime-guarded Tier 3 (lenient, so unguarded a + b is
not a hard error). Overflow is classified at the operands' common coerced
type (Int if either operand is Int, since Nat <: Int) — not one operand's
self-type, nor the possibly-narrowed result. Nat subtraction stays the
existing underflow obligation (E502).
Codegen emits explicit WASM overflow-detection guards (WASM wraps; there is
no native trap), trapping via unreachable; the precise overflow trap kind is
deferred to #808. The checker's resolved-type side-table is now threaded
into codegen so vera compile / vera run classify in lockstep with the
verifier.
Closes #798.
Co-Authored-By: Claude <noreply@anthropic.invalid>
|
Note Reviews pausedIt looks like this branch is under active development. To avoid overwhelming you with review comments due to an influx of new commits, CodeRabbit has automatically paused this review. You can configure this behavior by changing the Use the following commands to manage reviews:
Use the checkboxes below for quick actions:
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: ASSERTIVE Plan: Pro Run ID: 📒 Files selected for processing (1)
📝 WalkthroughWalkthroughThis PR adds integer-overflow obligations and runtime guards for ChangesInteger overflow soundness
Estimated code review effort🎯 5 (Critical) | ⏱️ ~90+ minutes Possibly related issues
Possibly related PRs
Suggested labels
🚥 Pre-merge checks | ✅ 4 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (4 passed)
✨ Finishing Touches🧪 Generate unit tests (beta)
Comment |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #809 +/- ##
==========================================
+ Coverage 91.95% 92.03% +0.07%
==========================================
Files 89 89
Lines 26684 26853 +169
Branches 321 321
==========================================
+ Hits 24537 24713 +176
+ Misses 2139 2132 -7
Partials 8 8
Flags with carried forward coverage won't be shown. Click here to find out more. ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 6
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@spec/06-contracts.md`:
- Around line 247-248: The E528 obligations table entry is too broad because it
implies `@Nat - `@Nat`` is included, while the verifier behavior keeps `@Nat`
subtraction under E502 only. Update the summary row in the contracts spec to
narrow the arithmetic covered by E528 or explicitly add the `@Nat - `@Nat``
exception, and make sure the wording stays consistent with the later paragraph
in the same section.
In `@spec/11-compilation.md`:
- Around line 56-57: The overflow paragraph needs to explicitly describe the
E528 verifier branch instead of folding it into the Tier-3 fallback. Update this
section to spell out the three cases in the verifier/codegen flow: proven
overflow raises E528 before codegen, solver-uncertain cases fall back to Tier 3
with guarded trapping ops, and proven-in-range cases emit the plain WASM op.
Make the classification key off the operands’ common coerced arithmetic type,
and reference the existing verification terminology so it matches the behavior
described elsewhere in the specification.
In `@TESTING.md`:
- Around line 9-13: The conformance program count is inconsistent across
TESTING.md, with the overview updated to 93 while another literal still says 92.
Update every remaining 92 in the document so all references match the new
conformance count, especially the later Conformance Suite prose that should
align with the table entry.
In `@tests/test_int_overflow_codegen.py`:
- Around line 43-67: The _compile_with_types helper only typechecks the direct
source and bypasses ModuleResolver, so it does not cover overflow classification
in imported bodies like cmd_run/cmd_compile do. Update this helper to mirror the
production import-resolution flow by resolving modules before codegen, then pass
the resulting artifacts through typecheck_with_artifacts and codegen_compile
using expr_semantic_types from the resolved compilation context. Keep the fix
centered on _compile_with_types and the imported-path setup so the suite
exercises cross-module overflow cases.
In `@tests/test_int_overflow_differential.py`:
- Around line 268-294: The narrowed `@Int-to-`@Nat overflow case is only covered
by verifier-only assertions and is missing from the parametrized
codegen-vs-verifier lockstep. Add this shape to _CORPUS so it is exercised
through _assert_in_lockstep, using the existing ContractVerifier and overflow
classification helpers to confirm the arithmetic width remains Int while the
result type is Nat.
In `@tests/test_int_overflow.py`:
- Around line 45-83: The overflow tests are too permissive because they only
check that at least one `int_overflow` obligation exists, so duplicate emissions
from the walker could still pass. Tighten the assertions in
`test_int_add_unbounded_emits_undischarged_overflow_obligation`,
`test_nat_add_unbounded_emits_undischarged_overflow_obligation`, and
`test_overflow_obligation_discharged_when_operands_bounded` by asserting the
exact overflow-obligation count or the exact `(kind, status)` sequence from
`result.obligations`, using the existing `_verify` helper and `ovf` filtering.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: bcbcd9b3-6219-40ec-9469-bd54178cbe52
⛔ Files ignored due to path filters (7)
docs/SKILL.mdis excluded by!docs/**docs/index.htmlis excluded by!docs/**docs/index.mdis excluded by!docs/**docs/llms-full.txtis excluded by!docs/**docs/llms.txtis excluded by!docs/**tests/conformance/ch04_int_overflow.verais excluded by!**/*.verauv.lockis excluded by!**/*.lock,!uv.lock
📒 Files selected for processing (30)
AGENTS.mdCHANGELOG.mdCLAUDE.mdFAQ.mdHISTORY.mdREADME.mdROADMAP.mdSKILL.mdTESTING.mdpyproject.tomlscripts/check_spec_examples.pyspec/06-contracts.mdspec/11-compilation.mdtests/conformance/manifest.jsontests/test_codegen.pytests/test_int_overflow.pytests/test_int_overflow_codegen.pytests/test_int_overflow_differential.pytests/test_verifier.pyvera/__init__.pyvera/cli.pyvera/codegen/api.pyvera/codegen/closures.pyvera/codegen/core.pyvera/codegen/functions.pyvera/errors.pyvera/obligations/core.pyvera/verifier.pyvera/wasm/context.pyvera/wasm/operators.py
… doc accuracy Round 2: adversarial-review + CodeRabbit findings on PR #809 (all tests/docs; no core-logic change). Tests: - Add the missing E528 'violated' regression (Int + Nat) — the loud-error arm of the two-check was untested; mutation-validated (disabling the branch flips it RED). Tighten the three existing obligation tests to assert the exact count. - Pin the Nat-subtraction exclusion at the real verifier gate (nat_sub, not int_overflow), not just the differential's re-derived helper. - Add the narrowed Int-into-Nat shape to the codegen/verifier lockstep corpus. - Cross-module coverage: thread ModuleResolver through the codegen helper (mirroring cmd_run) + a test that an imported function's overflow traps; mutation-validated against the guard hook. Docs: - spec/11 section 11.2.1: codegen is type-driven, not tier-driven — it emits the guard at every classified site regardless of the Z3 tier (fixed for both the overflow paragraph and the parallel Nat-subtraction paragraph); spell out the verifier three-way split (Tier 1 / E528 / Tier 3); drop the bare "(Option A)". - spec/06 section 6.4.3: narrow the E528 table row so Nat subtraction (E502) is not implied; fix the wrong "i64.MAX + 1" example (bare literals are Nat, in range) to "u64.MAX + 1". Same example fix in CHANGELOG. - TESTING.md: 92 -> 93 conformance count (3 stale mentions); refresh test counts (5145 -> 5151) across TESTING / README / ROADMAP. Refs #798. Co-Authored-By: Claude <noreply@anthropic.invalid>
Owner
Author
Review summary — adversarial multi-agent + CodeRabbitThe change was reviewed two independent ways:
All findings (deduped to 9 distinct items) are addressed in Test coverage
Doc accuracy
|
Owner
Author
|
@coderabbitai full review |
✅ Action performedFull review finished. |
There was a problem hiding this comment.
Actionable comments posted: 4
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@spec/11-compilation.md`:
- Around line 56-57: The subtraction summary in this section still overstates
the rule by implying non-@Nat subtraction sites are not obligation-checked,
which conflicts with the new `@Int/`@Nat overflow description. Update the
neighboring prose in the compilation spec so the follow-on sentence applies only
to `@Nat` subtraction underflow, while keeping the `@Int/`@Nat addition,
subtraction, and multiplication overflow handling described by the existing
arithmetic-obligation paragraph and its Tier 1/Tier 3 behavior.
In `@tests/test_int_overflow_codegen.py`:
- Around line 297-345: The overflow regression suite is missing coverage for the
special `@Nat` subtraction path, so add a small subtraction test block alongside
TestNatAddOverflow798 and TestNatMulOverflow798. Use the existing _assert_traps
and _assert_no_trap helpers with the `@Nat` subtraction opcode path (the
nat_sub/E502 behavior) to verify 0 - 1 traps and 5 - 3 stays in range. Keep the
new tests focused on the `@Nat` subtraction contract so codegen cannot silently
switch it to the new overflow-guarded arithmetic behavior.
In `@tests/test_int_overflow_differential.py`:
- Around line 323-343: The corpus sweep is skipping non-standalone files and
only checking binary sites from the entry AST, so imported-module arithmetic is
never compared. Update the test flow around typecheck_with_artifacts,
ContractVerifier, and _binary_sites to resolve imports via ModuleResolver
instead of pytest.skip, then collect and include binary sites from imported
modules in the mismatch loop so the lockstep check covers cross-module cases
too.
In `@tests/test_int_overflow.py`:
- Around line 108-119: The Nat ceiling overflow test currently only checks the
violated `int_overflow` obligation in
`test_nat_overflow_obligation_violated_at_u64_ceiling`, so extend it to also
assert the user-facing `E528` diagnostic for this `@Nat` path. Reuse the same
diagnostic-checking pattern already used in the signed-ceiling overflow test,
and verify the public verifier output alongside the existing
`result.obligations` assertions so the Nat branch covers both internal and
external surfaces.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: a21b47bf-6034-4006-9f71-aeb4c6290784
⛔ Files ignored due to path filters (7)
docs/SKILL.mdis excluded by!docs/**docs/index.htmlis excluded by!docs/**docs/index.mdis excluded by!docs/**docs/llms-full.txtis excluded by!docs/**docs/llms.txtis excluded by!docs/**tests/conformance/ch04_int_overflow.verais excluded by!**/*.verauv.lockis excluded by!**/*.lock,!uv.lock
📒 Files selected for processing (30)
AGENTS.mdCHANGELOG.mdCLAUDE.mdFAQ.mdHISTORY.mdREADME.mdROADMAP.mdSKILL.mdTESTING.mdpyproject.tomlscripts/check_spec_examples.pyspec/06-contracts.mdspec/11-compilation.mdtests/conformance/manifest.jsontests/test_codegen.pytests/test_int_overflow.pytests/test_int_overflow_codegen.pytests/test_int_overflow_differential.pytests/test_verifier.pyvera/__init__.pyvera/cli.pyvera/codegen/api.pyvera/codegen/closures.pyvera/codegen/core.pyvera/codegen/functions.pyvera/errors.pyvera/obligations/core.pyvera/verifier.pyvera/wasm/context.pyvera/wasm/operators.py
…oss-module test coverage Round 3: 4 CodeRabbit findings on PR #809 (all tests/docs; no core-logic change). - spec/11 section 11.2.1: scope the "Int - Int not obligation-checked" sentence to the *underflow* obligation and cross-reference the overflow obligation above — the flat wording contradicted the new overflow paragraph. - tests/test_int_overflow.py: assert the user-facing E528 diagnostic on the Nat ceiling test too (it only checked the obligation), mirroring the Int test. - tests/test_int_overflow_codegen.py: add TestNatSubUnderflow798 pinning that Nat subtraction stays the #520 nat_sub underflow guard, not #798 overflow arithmetic. CR's suggested "0 - 1" example is exempt (pure literals don't trap); the tests use slot provenance (3 - 5 traps, 5 - 3 = 2). - tests/test_int_overflow_differential.py: cover cross-module arithmetic by sweeping imported *_lib.vera modules STANDALONE. CR's suggested fix (resolve imports in the consumer + include imported sites) is a false positive: the verifier obligates per-module, so verifier-of-consumer (None) vs codegen-of-imported-body (Int) is a category mismatch, not a desync. Swept standalone, the lib's sites are in lockstep. Doc counts refreshed (5151 -> 5156). Refs #798. Co-Authored-By: Claude <noreply@anthropic.invalid>
There was a problem hiding this comment.
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
spec/11-compilation.md (1)
46-58: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winSynchronise §11.3.3 with the always-guarded
@Natsubtraction rule.This subsection now correctly says the
@Nat -@Nat`` guard is emitted regardless of verifier tier, but Line 109 still says a discharged site compiles to barei64.sub. That leaves the spec internally inconsistent on the same codegen path. Please update the later operator note so Tier 1 means “guard proven unreachable”, not “unguarded op emitted”. Based on learnings, "`Nat` subtraction guards and `Int`/`Nat` overflow guards are type-driven rather than tier-driven". As per path instructions, "Review Markdown files for factual accuracy against the codebase".🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@spec/11-compilation.md` around lines 46 - 58, The §11.3.3 operator note is inconsistent with the always-guarded `@Nat - `@Nat`` codegen path described in the same section. Update the subtraction/overflow wording in this spec text so Tier 1 means the guard is proven unreachable, not that `i64.sub` is emitted without a guard, and keep the explanation aligned with the `@Nat` subtraction and arithmetic overflow rules referenced in the surrounding prose.Sources: Path instructions, Learnings
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Outside diff comments:
In `@spec/11-compilation.md`:
- Around line 46-58: The §11.3.3 operator note is inconsistent with the
always-guarded `@Nat - `@Nat`` codegen path described in the same section. Update
the subtraction/overflow wording in this spec text so Tier 1 means the guard is
proven unreachable, not that `i64.sub` is emitted without a guard, and keep the
explanation aligned with the `@Nat` subtraction and arithmetic overflow rules
referenced in the surrounding prose.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: aad6426d-bbe6-4488-943b-74ba2799c14f
📒 Files selected for processing (7)
README.mdROADMAP.mdTESTING.mdspec/11-compilation.mdtests/test_int_overflow.pytests/test_int_overflow_codegen.pytests/test_int_overflow_differential.py
…iven codegen Addresses a CodeRabbit outside-diff finding on PR #809: section 11.3.3 still said a Z3-discharged Nat subtraction compiles to a bare i64.sub, contradicting the section 11.2.1 rule (corrected earlier this PR) that the underflow guard is emitted regardless of the verifier's tier. Reworded: the bare i64.sub applies only at guard-exempt sites (pure-literal subtractions); where the guard applies it is emitted type-driven (a Tier-1 discharge means it provably never fires, not that it is omitted). Refs #798. Co-Authored-By: Claude <noreply@anthropic.invalid>
Owner
Author
|
@coderabbitai The outside-diff finding on |
|
Tip For best results, initiate chat on the files or code changes.
The rewording for ✏️ Learnings added
|
There was a problem hiding this comment.
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
spec/11-compilation.md (1)
46-56: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winUse
i64consistently here
@Intand@Natboth compile toi64in §11.2.1, so thei64/u64wording is off. The lead-in should also be narrowed to the underflow-specific@Nat -@Nat`` case now that+, `-`, and `*` all have overflow obligations.Suggested tweak
- The one operation that can violate the invariant despite well-typed operands is unsigned subtraction (`@Nat - `@Nat``). + The underflow-specific case is unsigned subtraction (`@Nat - `@Nat``). - ... (`@Int` (i64) if either operand is `@Int`, else `@Nat` (u64); `@Nat` subtraction is excluded, being the underflow obligation above). + ... (`@Int` if either operand is `@Int`, else `@Nat`; `@Nat` subtraction is excluded, being the underflow obligation above).🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@spec/11-compilation.md` around lines 46 - 56, The §11.2.1 arithmetic wording is inconsistent: `@Int` and `@Nat` both lower to `i64`, so remove the `i64/u64` split and describe the common representation as `i64` throughout. Also narrow the lead-in to the underflow-specific `@Nat - `@Nat`` case, since the overflow discussion for `+`, `-`, and `*` should be described separately. Update the relevant text in the compilation spec section that mentions the subtraction obligation and the common arithmetic type so it matches the `@Int`/`@Nat` lowering used by the compiler.Source: Path instructions
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Outside diff comments:
In `@spec/11-compilation.md`:
- Around line 46-56: The §11.2.1 arithmetic wording is inconsistent: `@Int` and
`@Nat` both lower to `i64`, so remove the `i64/u64` split and describe the
common representation as `i64` throughout. Also narrow the lead-in to the
underflow-specific `@Nat - `@Nat`` case, since the overflow discussion for `+`,
`-`, and `*` should be described separately. Update the relevant text in the
compilation spec section that mentions the subtraction obligation and the common
arithmetic type so it matches the `@Int`/`@Nat` lowering used by the compiler.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: 4e7e25f7-d699-44d3-8402-20d5f8a2af79
📒 Files selected for processing (1)
spec/11-compilation.md
…gned/unsigned 64-bit) Addresses a second CodeRabbit outside-diff finding on PR #809: section 11.2.1 said Int/Nat "share the i64/u64 representation", contradicting the section's own opening ("share the same WASM representation (i64)"). Both lower to i64; the u64 is the unsigned interpretation/range, not a separate representation. - Representation: both are i64 (one WASM type). - Overflow range: signed 64-bit for Int, unsigned 64-bit for Nat — the load-bearing distinction (the verifier uses I64_MIN/I64_MAX vs 0/U64_MAX), now stated as a range, separate from representation. - Scoped the lead-in to the *non-negativity* invariant so the underflow (Nat - Nat) discussion reads as distinct from the overflow discussion below. Refs #798. Co-Authored-By: Claude <noreply@anthropic.invalid>
Owner
Author
|
@coderabbitai The §11.2.1 representation/range finding is fixed in |
|
Tip For best results, initiate chat on the files or code changes.
The revised wording makes the distinction precise: ✏️ Learnings added
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #798 — batch 4 of the #392
smt.pysoundness audit.The bug
vera verifymodelled@Int/@Natas Z3's unbounded integers, so+/-/*were treated as total — it proved postconditions the i64 / u64 runtime then violated under two's-complement wraparound:vera verify→ proved for all inputs, yetvera run inc -- 9223372036854775807(i64.MAX) wrapsx + 1toi64.MIN < x. Overflow was the one partial-arithmetic case treated as total by both tiers (@Natunderflow and signed-divMIN/-1already trap).The fix (a language-semantics decision — trap-on-overflow, approved)
@Int/@Nat+/-/*are now partial operations that trap on overflow at runtime, and the verifier auto-synthesises anint_overflowobligation that the result stays in i64 / u64 range:vera/verifier.py): a two-check mirroring array bounds (Auto-inject obligations for primitive operations (division, modulo, array index) to match README's static-safety claim #680) — provably in range → Tier 1; provably out of range (i64.MAX + 1) → loud E528; dynamic operands → runtime-guarded Tier 3. Lenient (tier3-by-default), so unguardeda + bis not a hard error.vera/wasm/operators.py): an explicit overflow-detection guard per op (WASM wraps; there is no native trap) — signed-i64 sign tests for Int add/sub, a division round-trip witha==0+a==-1 && b==INT_MINpre-checks for Int mul (dodging the nativediv_strap), unsigned carry/round-trip for Nat add/mul. Traps viaunreachable(the preciseoverflowkind is deferred — see below).@Intif either operand is@Int(since@Nat <: @Int), else@Nat. This is not one operand's self-type (a non-negative literal is@Nat, but5 + @Int.0is an i64 add) nor the possibly-narrowed result (@Int.0 + 1stored into a@Natslot is still an i64 add). Verifier and codegen share this rule in lockstep.@Natsubtraction is excluded — it stays the existing underflow obligation (E502).Exit checklist (§0)
pytest tests/— green (5124 passed, 16 skipped, 16 deselected)mypy vera/— cleancheck_conformance.py— 93/93 (newch04_int_overflow.vera, all sites Tier-1)check_examples.py— 35/35 (check+verify)check_version_sync.py— 0.0.181[0.0.181]+ link refs; doc-counts / site-assets / spec-examples greentests/test_int_overflow.py(RED-confirmed)Verification (test-first + adversarial)
codegen-traps(a*b) ⟺ Python's exact product out of range, 0 mismatches.tests/test_int_overflow_differential.py): the set ofint_overflow-obligated sites == the set of codegen-guarded sites, swept across every example + verify/run conformance program.Notable change
To classify in lockstep, the checker's resolved-type side-table is now threaded into codegen (
vera/wasm/context.py,vera/codegen/{api,core,functions,closures}.py,vera/cli.py), sovera compile/vera runconsult the same resolved type the verifier does.Deferred (sound, tracked)
overflowruntime trap kind (the guard currently traps with the genericunreachablekind, like the Nat subtraction silently underflows to negative i64 — refinement-type soundness hole #520 underflow story; the precise diagnostic path isvera verify+ E528). Needs host-import scaffolding; same deferral as@Natunderflow's dedicated kind.🤖 Generated with Claude Code
Summary by CodeRabbit
@Int/@Natarithmetic overflow obligations for+,-, and*, with dynamic overflow enforced by runtime traps.@Natsubtraction behaviour.